Inference at * 
Iof proof for Lemma p-first-singleton:


  A, B:Type, f:(A(B + Top)). p-first([f]) = f 

latex

 by ((Auto) 
CollapseTHEN (((Ext) 
CollapseTHEN (((Auto) 
CollapseTHEN (((Unfold `p-first` 0) 

CoCollapseTHEN (((Reduce 0) 
CollapseTHEN (Auto)))))))))) 

latex

Co.

Definitions

Type, x:A. B(x), x:AB(x), s = t, left + right, Top, p-first(L), f(a)